\begin{tabbing}
ecl{-}trans{-}normal($x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=let $T$,${\it ks}$,$i$,$g$,$h$,$a$,$e$ = $x$ in \+
\\[0ex]($\forall$$x$, $y$:$T$. Dec($x$ $=$ $y$)) \& ($\forall$$n$:$\mathbb{N}$. $\neg$$h$($n$,$i$))
\\[0ex]\& finite{-}type($T$)
\\[0ex]\& sorted($e$)
\\[0ex]\& no\_repeats($\mathbb{N}^{+}$;$e$)
\-
\end{tabbing}